(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^2).
The TRS R consists of the following rules:
rev(nil) → nil
rev(.(x, y)) → ++(rev(y), .(x, nil))
car(.(x, y)) → x
cdr(.(x, y)) → y
null(nil) → true
null(.(x, y)) → false
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
rev(nil) → nil
rev(.(z0, z1)) → ++(rev(z1), .(z0, nil))
car(.(z0, z1)) → z0
cdr(.(z0, z1)) → z1
null(nil) → true
null(.(z0, z1)) → false
++(nil, z0) → z0
++(.(z0, z1), z2) → .(z0, ++(z1, z2))
Tuples:
REV(nil) → c
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) → c2
CDR(.(z0, z1)) → c3
NULL(nil) → c4
NULL(.(z0, z1)) → c5
++'(nil, z0) → c6
++'(.(z0, z1), z2) → c7(++'(z1, z2))
S tuples:
REV(nil) → c
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
CAR(.(z0, z1)) → c2
CDR(.(z0, z1)) → c3
NULL(nil) → c4
NULL(.(z0, z1)) → c5
++'(nil, z0) → c6
++'(.(z0, z1), z2) → c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:
rev, car, cdr, null, ++
Defined Pair Symbols:
REV, CAR, CDR, NULL, ++'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 6 trailing nodes:
++'(nil, z0) → c6
CDR(.(z0, z1)) → c3
REV(nil) → c
NULL(nil) → c4
CAR(.(z0, z1)) → c2
NULL(.(z0, z1)) → c5
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
rev(nil) → nil
rev(.(z0, z1)) → ++(rev(z1), .(z0, nil))
car(.(z0, z1)) → z0
cdr(.(z0, z1)) → z1
null(nil) → true
null(.(z0, z1)) → false
++(nil, z0) → z0
++(.(z0, z1), z2) → .(z0, ++(z1, z2))
Tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
S tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:
rev, car, cdr, null, ++
Defined Pair Symbols:
REV, ++'
Compound Symbols:
c1, c7
(5) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
car(.(z0, z1)) → z0
cdr(.(z0, z1)) → z1
null(nil) → true
null(.(z0, z1)) → false
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
rev(nil) → nil
rev(.(z0, z1)) → ++(rev(z1), .(z0, nil))
++(nil, z0) → z0
++(.(z0, z1), z2) → .(z0, ++(z1, z2))
Tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
S tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
K tuples:none
Defined Rule Symbols:
rev, ++
Defined Pair Symbols:
REV, ++'
Compound Symbols:
c1, c7
(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
We considered the (Usable) Rules:none
And the Tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(++(x1, x2)) = 0
POL(++'(x1, x2)) = 0
POL(.(x1, x2)) = [1] + x2
POL(REV(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c7(x1)) = x1
POL(nil) = 0
POL(rev(x1)) = 0
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
rev(nil) → nil
rev(.(z0, z1)) → ++(rev(z1), .(z0, nil))
++(nil, z0) → z0
++(.(z0, z1), z2) → .(z0, ++(z1, z2))
Tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
S tuples:
++'(.(z0, z1), z2) → c7(++'(z1, z2))
K tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
Defined Rule Symbols:
rev, ++
Defined Pair Symbols:
REV, ++'
Compound Symbols:
c1, c7
(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
++'(.(z0, z1), z2) → c7(++'(z1, z2))
We considered the (Usable) Rules:
rev(.(z0, z1)) → ++(rev(z1), .(z0, nil))
++(.(z0, z1), z2) → .(z0, ++(z1, z2))
rev(nil) → nil
++(nil, z0) → z0
And the Tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(++(x1, x2)) = x1 + [2]x2
POL(++'(x1, x2)) = [1] + [2]x1
POL(.(x1, x2)) = [2] + x2
POL(REV(x1)) = x12
POL(c1(x1, x2)) = x1 + x2
POL(c7(x1)) = x1
POL(nil) = 0
POL(rev(x1)) = [2]x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
rev(nil) → nil
rev(.(z0, z1)) → ++(rev(z1), .(z0, nil))
++(nil, z0) → z0
++(.(z0, z1), z2) → .(z0, ++(z1, z2))
Tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
S tuples:none
K tuples:
REV(.(z0, z1)) → c1(++'(rev(z1), .(z0, nil)), REV(z1))
++'(.(z0, z1), z2) → c7(++'(z1, z2))
Defined Rule Symbols:
rev, ++
Defined Pair Symbols:
REV, ++'
Compound Symbols:
c1, c7
(11) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(12) BOUNDS(1, 1)